Nuprl Lemma : sq_stable__eqfun_p
13,42
postcript
pdf
T
:Type,
eq
:(
T
T
). SqStable(IsEqFun(
T
;
eq
))
latex
Up
rel
1
,
rel
1
Definitions
P
Q
,
P
Q
,
P
&
Q
,
x
f
y
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
t
T
Lemmas
bool
wf
,
assert
wf
,
iff
wf
origin
T:Type, eq:(T
T
). SqStable(IsEqFun(T;eq)) T:Type, eq:(TT). SqStable(IsEqFun(T;eq)) 
Q
Q Qx:A. B(x)
T